Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a(a(f(x,y)))  → f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
2:    f(a(x),a(y))  → a(f(x,y))
3:    f(b(x),b(y))  → b(f(x,y))
There are 10 dependency pairs:
4:    A(a(f(x,y)))  → F(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
5:    A(a(f(x,y)))  → A(b(a(b(a(x)))))
6:    A(a(f(x,y)))  → A(b(a(x)))
7:    A(a(f(x,y)))  → A(x)
8:    A(a(f(x,y)))  → A(b(a(b(a(y)))))
9:    A(a(f(x,y)))  → A(b(a(y)))
10:    A(a(f(x,y)))  → A(y)
11:    F(a(x),a(y))  → A(f(x,y))
12:    F(a(x),a(y))  → F(x,y)
13:    F(b(x),b(y))  → F(x,y)
The approximated dependency graph contains one SCC: {4,7,10-13}.
Tyrolean Termination Tool  (0.24 seconds)   ---  May 3, 2006